Section: New Results

Formal Verification of Transformations on Abstract Clock in Synchronous Compilers

Participants : Van-Chan Ngo, Jean-Pierre Talpin, Paul Le Guernic.

Translation validation was introduced in the 90's by Pnueli et al. as a technique to formally verify the correctness of code generated from the data-flow synchronous language Signal using model checking. Rather than certifying the code generator (by writing it entirely using a theorem prover) or qualifying it (by obeying to the 27 documentations required as per the DO-178C), translation validation provides a scalable approach to assessing the functional correctness of automatically generated code. By revisiting translation validation, which in the 90's suffered from the limitations of theorem proving and model checking techniques available then, we aim at developing a scalable and flexible approach that applies to the existing 500k-lines implementation of Signal, Polychrony, and is capable of handling large-scale, possibly automatically generated, Signal programs, while using of-the-shelf, efficient, model-checkers and Sat/Smt -solving libraries [36] , [63] .

The abstract clock semantics of polychronous equations is formalized as a first-order logic formula over boolean variables. For a signal $x$, if $x$ is boolean then we use two boolean variables $x$, and $\widehat{x}$ to represent the value of signal $x$ and it abstract clock, respectively. If $x$ is non-boolean signal, we only need to capture its abstract clock by a boolean variable $\widehat{x}$. The boolean variable $\widehat{x}$ is true when the signal $x$ is present and otherwise it is absent. The equational structure of a synchronous data-flow language makes that it is natural to represent the relations between abstract clocks described implicitly or explicitly by equations in terms of first-order logic formulas. And then the combination of equations can be represented by the conjunction of the corresponding first-order logic formulas. We assume that all considered programs are supposed to be written with the primitive operators, meaning that derived operators are replaced by their corresponding primitive ones, and there is no nested operators such as $z:=x\text{default}\left(y\text{when}b\right)$. The nested operators are broken by using fresh variables. These formulas use the usual logic operators and numerical comparison functions. Consider a general equation $y:=R(x_1,x_2,...,x_n)$, where $R$ is an operator defined in a synchronous language (e.g. suspend in Esterel, when in Signal...), or it can be a usual boolean or numerical operator, then the abstract clock semantics of this equation can be represented as a first-order logic formula over the clocks and/or the boolean value of the involved signals $\Phi (\widehat{y},\widehat{x_1},\widehat{x_2},...,\widehat{x_n},x_1,...)$. For a boolean expression defined by numerical comparison functions and numerical expressions, to ensure the result formulas are boolean, we only encode the fact that the clocks of boolean and numerical expressions are synchronized, and we avoid encoding the numerical comparison function which defines the value of the boolean expression and the numerical expressions. For each $i^{th}$ equation in program $P$, we denote by ${\Phi }_{e{q}_i}$ its abstract clock semantics, then the abstract clock semantics of $P$ can be represented by a first-order logic formula, called its clock model, denoted as:

where $n$ denotes the number of equations composed in $P$. The detailed encoding scheme of the Signal language can be found in [19] .

Given two clock models $P_1$ and $P_2$, we say that $P_2$ is a correct transformation on abstract clocks of $P_1$, or $P_2$ refines $P_1$ w.r.t the clock semantics, if it satisfies:

We write $P_2{⊑}_{clock}{P}_1$ to denote the fact that $P_2$ refines $P_1$. We also provide an approach to check the existence of refinement by using a Smt -solver that is based on the following theorem:

Theorem. Given a source program $P_1$ and its transformed program $P_2$, $P_2$ is a correct transformation of $P_1$ on abstract clocks if it satisfies that the formula ${\Phi }_{P_1}$ is a logical consequence of the formula ${\Phi }_{P_2}$, or

Here, we delegate the checking of the above formula against the clock models to a Smt -solver that efficiently deals with first-order logic formulas over boolean and numeric expressions. The checking formulas belong to decidable theories, this solver gives two types of answers: sat when the formula has a model (there exists an interpretation that satisfies it); or unsat otherwise. Our implementation uses the Smtlib common format [31] to encode the formulas obtained from the previous step as input of Smt solvers. For our implementation, we consider the Yices solver [38] , which is one of the best two solvers at the last Smtcomp competition [59] .